型システム入門 プログラミング言語と型の理論
https://gyazo.com/e24ca4823f970464c63f9b74785a87b5
著者のおすすめ読み方のスライド
第1章 はじめに
if <複雑な条件> then 5 else <型エラー>
このようなプログラムでは、正しく型付けすることはできない。静的解析では判断できない 型システムでなにができるのか
エラーの検出
抽象化
ドキュメント化
言語の安全性
安全な言語とはプログラミングの最中にうっかり自分の足を撃つことが不可能な言語であると定義できる
静的型安全性と言語の安全性はイコールではない
脱出用ハッチを準備していることは多い。
効率性
高性能なコンパイラは最適化もできるし協力な型検査もできる 第2章 数学的準備
■第1部 型無しの計算体系
第3章 型無し算術式
「t ::=項： true定数真 false定数偽 if t then t else t条件式 0定数ゼロ succ t後者値 pred t前者値 iszero tゼロ判定 」
この記法は全体で使う
項がどう評価されるかについては意味論の正確な定義が必要 評価は必ずどれか1つになるはずなのが数学的に証明されているためt→t`は成り立つ
当てはまる規則がないこと
しかし正常に次の状態に遷移できないつまり正規形ではないことについても確認しないといけない
if true then 1 else x11
これは正規形なのでプログラムが正常に行われる
if 1 then 2 else 3
これは型システム的には不正である1は本来Boolean型でないといけないので数値と評価している
このときが行き詰まり状態。つまりエラーになっている
第4章 算術式のML実装
第5章 型無しラムダ計算
λx.t ラムダ抽象
t t 関数適用
抽象構文と具象構文
具象構文はいわゆる人間（またはAI）が書くコード
抽象構文は単純な内部的表現（機械語？といっていいいんだろうか）ASTとして表現されるもの 字句解析器によってプログラマが書いたコードを識別子や予約後、定数、区切り文字などのトークンにする 構文解析器がトークンの列を抽象構文木ASTに変換する このときに様々なルールがある、優先順位や結合法則
例えば掛け算と足し算では掛け算のほうが優先になる。
関数適用は、左結合になり、抽象の本体は右側へ拡大していく
スコープ
λx . tのxは束縛された状態を指す（束縛子）
x yやλy, xyなどのxは束縛されていない（自由である）
まあローカル変数かグローバル変数みたいな感じかなrkasu.icon
プログラムがどのように実行されるかをステップごとに示す
プログラムがどのように評価・実行されるかを逐次的なステップとして記述する方法
β簡約は、関数適用（function application）の評価ルール
即時実行
非正格な戦略をとっているか
遅延実行
引数が本当に必要なときしか実行されない
ラムダ計算でのプログラミング
複数の引数はラムダ計算ではサポートしていないがカリー化で評価実行することができる f = λx.λy.s というのは f=(x) => (y) => sみたいな感じ
Churchブール値
基本難しくないかも
tureなら1つ目を返す、falseなら2つ目を返すみたいな感じ
Church数
足し算というか加算でかなりの簡約が必要
掛け算の場合は部分適用する
times = λn . λm. m (plus n) c0
Xをn回やるというコンビネーター
減算は足し算より難しい
第6章 項の名無し表現
第7章 ラムダ計算のML実装
■第2部 単純型
第8章 型付き算術式
第9章 単純型付きラムダ計算
第10章 単純型のML実装
第11章 単純な拡張
第12章 正規化
第13章 参照
第14章 例外
■第3部 部分型付け
第15章 部分型付け
第16章 部分型付けのメタ理論
第17章 部分型付けのML実装
第18章 事例：命令的オブジェクト
第19章 事例：Featherweight Java
■第4部 再帰型
第20章 再帰型
第21章 再帰型のメタ理論
■第5部 多相性
第22章 型再構築
第23章 全称型
第24章 存在型
第25章 System F のML実装
第26章 有界量化
第27章 事例：命令的オブジェクト再考
第28章 有界量化のメタ理論
■第6部 高階の型システム
第29章 型演算子とカインド
第30章 高階多相
第31章 高階部分型付け
第32章 事例：純粋関数的オブジェクト
付録A 演習の解答
付録B 記法
参考文献
訳語集
規則図一覧
索引